(declare-fun a () Real)
(declare-fun b () Real)
(declare-fun c () Real)
(assert (let ((?v_4 (<= 0 b))(?v_2 0)) (let ((?v_1 0)(?v_0 0)(?v_3 (* a (- 1)))) (let ((?v_5 (* a ?v_3))) (let ((?v_6 0)) (and ?v_4 (and (<= (* c (+ (+ (/ 471 100) (* a (+ (- 3) (* a (/ 157 100))))) (* b (+ (+ (- 3) (* a (+ (/ (- 471) 100) (* a (+ 2 ?v_0))))) (* b (* a ?v_1)))))) (+ (+ 3 (* a (+ (/ (- 471) 100) (* a (+ 4 ? v_0))))) (* b (+ (+ (/ (- 471) 100) (* a (+ 3 ?v_0))) (* b ? v_1))))) (and (not (<= 0 a)) (and (not (<= ? v_2 (- 3))) (and (not (<= (* c (+ 1 (* b ?v_3))) (+ ?v_3 (* b (- 1))))) (and (or (not ?v_4) (or (<= (* c (+ (- 1) (* b a))) (+ a b)) (<= (* c (+ ?v_1 ?v_6)) (+ (* a ?v_5) (* b (+ (* a (* a (- 3))) ?v_6)))))) (and (not (<= c 0)) (and (not (<= a (- 1))) (and (not (<= 1 b)) (not (<= b a))))))))))))))))
(check-sat)
